constR{$x:ut2}(T; c; i) == ([@i "$x" initially c:T; @i only events in nil change "$x":T]) 

latex

---

clarification:

constR{$x:ut2}(T; c; i) == (@i "$x" initially c:T.@i only events in nil change "$x":T.nil) 

latex

Definitions

(L), @loc x initially v:T, car.cdr, @loc only events in L change x:T, "$x", nil